A, B:Type, R:(AA), S:(BB), opa:(AA), opb:(BB), f:(AB).
fun_thru_1op(A;B;opa;opb;f)
 RelsIso(A;B;x,y.R(x,y);x,y.S(x,y);f)
 monot(B;x,y.S(x,y);opb)
 monot(A;x,y.R(x,y);opa) 

latex

Up	gen algebra 1
Definitions of Statement	fun_thru_1op(A;B;opa;opb;f), monot(T;x,y.R(x;y);f), RelsIso(T;T';x,y.R(x;y);x,y.R'(x;y);f)
Definitions	x,y. t(x;y), t  T, monot(T;x,y.R(x;y);f), x(s1,s2), P  Q, , x:A. B(x), P & Q, P  Q, P  Q, RelsIso(T;T';x,y.R(x;y);x,y.R'(x;y);f), fun_thru_1op(A;B;opa;opb;f)
Lemmas	fun thru 1op wf, rels iso wf, monot wf, iff transitivity